es:ES, T:Type, i:Id, P:(TProp), Q:(ETProp).
(x:T. Dec(P(x)))
 (L:T List.
 ((xL. e:E. Q(e,x)  loc(e) = i  Id)
 ( (xL. P(x)  (e:E. Q(e,x)))
 ( ((xL.P(x))  e'@i.True)
 ( e'@i.xL. P(x)  (e:E. e  e'  & Q(e,x))) 

latex

Definitions	Dec(P), x(s), ES, False, x:A. B(x), A & B, e  e' , x(s1,s2), A, (xL.P(x)), e@i.P(e), x. t(x), True, E, Id, loc(e), xL. P(x), (x  l), P  Q, P & Q, P  Q, {T}, P  Q, Prop, x:A. B(x), t  T, P  Q, {i..j}, i  j < k, AB, l[i], ij, i<j, hd(l), ij, ||as||, (e <loc e'), Trans x,y:T. E(x;y)
Lemmas	l exists wf, es-le-trans, es-locl wf, es-le-total, length wf1, non neg length, le wf, select member, cons member, l member wf, es-loc wf, Id wf, es-E wf, true wf, existse-at wf, not wf, l exists cons, not functionality wrt iff, implies functionality wrt iff, es-le wf, l all wf, l all nil, false wf, l exists nil, decidable wf, event system wf